A:Type, d1,d2,d3,d4:EqDecider(A), B:(AType), f,g:fpf(A; a.B(a)), x:A, z:B(x).
fpf-sub(A; a.B(a); d4; f; g)
 (fpf-dom(d3; x; f))
 (fpf-cap(f; d1; x; z) = fpf-cap(g; d2; x; z)  B(x)) 

latex

Definitions	x:A. B(x), x(s), P  Q, fpf-cap(f; eq; x; z), if b then t else f fi , t  T, tt, x. t(x), ff, prop{i:l}, top, , Unit, P  Q, P  Q, fpf-sub(A; a.B(a); eq; f; g), A c B, guard(T), A, False,
Lemmas	fpf-dom wf, bool wf, eqtt to assert, fpf-trivial-subtype-top, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, fpf-sub wf, fpf wf, deq wf, fpf-dom functionality2, fpf-ap functionality